[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
MASTERARBEIT
Titel der Masterarbeit
On Hilbert’s Tenth Problem over
Rings of Algebraic Integers
verfasst von
Tim Benedikt Herbstrith BSc
angestrebter akademischer Grad
Master of Science (MSc)
Wien, 2019
Studienkennzahl lt. Studienblatt: A 033 821
Studienrichtung lt. Studienblatt: Mathematik
Betreut von: ao. Univ.-Prof. Mag. Dr. Ch. Baxa
[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
                  
         
                  
               
             
https://github.com/tim6her/h10-over-rings-of-integers
Some Rights
Reserved
[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
Contents
1 Prerequisites and central notions 1
    
     
        
     
    
     
      
     
        
  

    
      
2 Hilbert’s tenth problem 57
       
     
    
   
    
               
     
     
A Collected Haskell implementations 103
    
  
B Summaries 111
  
  

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
1 Prerequisites and central notions
                
                  
              
             
           
              
                
             
               
              
               
               

           

1.1 Prerequisites from computability theory
            
          
            

              
            
                
             
           
              
            
                
          
                
              
               
               
         
[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
2
1 3
3
1
2
𝑥 = 101
𝑦 = 011
       
1.1.1 Turing machines, problems, and decidability
      01 01
    
           01   
  0  1   
               
         
          

                
              
 
         

              
               
         
 











             
               

1 
           
     
101  011       
[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    
         
                
             
                 
                   
          §             
          _      
  
      §_01    
           
start
halt
 

    
     
 §     §
  §   
 
halt

halt

                
                 
               
                 
   
       §          
              
     
halt
          
 
                   
    0           
 0    
overow
  

overow
0
return
1
             
return
 
 1                  
    
overow
0          
               
 
         
              
  
[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
§
0 0 0 1
. . .
overflow
   
    
halt
        

start
  §       _    
        
§__
              
                
 
§001_0__
              
01

      


        

§ 


_ 
   
      
 

  
      
 



 
             
               
 
start
            

halt
              
  
         
delta

state

state’

  
delta "state" b = ("state'", b', m)
            
               
     
[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    
         
-- start by entering the "overflow" state ...
add1 "start" '§' = ("overflow", '§', 1 )
-- ... and stay in this state, as long as you read only '1'-s
add1 "overflow" '1' = ("overflow", '0', 1 )
-- if you read the first '0' or an empty cell replace it by '1'
-- and enter the "return" state to move the head to the first cell
add1 "overflow" '0' = ("return", '1', -1)
add1 "overflow" '_' = ("return", '1', -1)
-- we finish if we read '§' again or ...
add1 "return" '§' = ("halt", '§', 0 )
-- ... continue to move to the left and don't change the cell
-- content. Here `b` matches '0' or '1'
add1 "return" b = ("return", b , -1)
add1 _state _char = ("error", '_', 0 )
delta "state" 1 = ("state'", b', m )
delta "state" b = ("state''", b'', m')
   


state’


state
1

state”


state
1
              
              

1
           
     
add1

start
halt
overow
return
error

add1

           
                  
              
error
   
add1
 1101          
         1101     
    
             
       
     1     0
    01
        
          
1
 https://www.haskell.org/onlinereport/haskell2010
[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
§
1 1 0 1
. . .
start
 
start
§
overow
§
§
1 1 0 1
. . .
overflow
 
overow
1
overow
0
§
0 1 0 1
. . .
overflow
 
overow
1
overow
0
§
0 0 0 1
. . .
overflow
 
overow
0
return
1
§
0 0 1 1
. . .
return
 
return
0
return
0
§
0 0 1 1
. . .
return
 
return
0
return
0
§
0 0 1 1
. . .
return
 
return
§
halt
§
§
0 0 1 1
. . .
halt
 
halt
§
halt
§
     
add1
 1101
[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    
  01
      
  
            
      
               
            

               
         
start
halt
accept
reject




           

start

      


1


1
1 

reject
_ 


0


0
0 

reject
_ 


_

accept
_  


reject
_  

                

    


                  
               
             
        
     _            
    
                
       
        

  

accept
        1   
reject
  
    0  
[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
                 
       
accept

reject
    
              
    
                

  



     

 
     
 

   


 


 
start
halt
 
 
     
     

start
§
halt
§ 
    
   

            



  

start
halt


start
halt
 
start
halt
compose
          
 

 
start

compose
 


halt

 
halt

start
 
compose



        
 
     
      
   
11
-times
 

     






1 
0
[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    
        
-- start by entering the "check" state and ...
tally "start" '§' = ("check", '§', 1 )
-- ... stay in this state while reading only '1'-s
tally "check" '1' = ("check", '1', 1 )
-- on reading '_' accept the input and clear the tape ...
tally "check" '_' = ("accept", '_', -1)
tally "accept" '1' = ("accept", '_', -1)
-- ...except for cell c(1), where you write a '1'
tally "accept" '§' = ("accept", '§', 1 )
tally "accept" '_' = ("halt", '1', -1)
-- however, if you read a '0' first, reject the input
-- by moving to the end of the input string ...
tally "check" '0' = ("rejectMR", '0', 1 )
tally "rejectMR" '_' = ("reject", '_', -1)
tally "rejectMR" b = ("rejectMR", b, 1 ) -- `b` matches '0' or '1'
-- ... and clear the tape except for cell c(1) where you
-- write a '0'
tally "reject" '§' = ("reject", '§', 1 )
tally "reject" '_' = ("halt", '0', -1)
tally "reject" b = ("reject", '_', -1) -- `b` matches '0' or '1'
tally _state _char = ("error", '_', 0 )
         




 

            01
  

    
01
    
                  
        
01
                  
            1     
  
tally

start
halt
check
accept
reject
rejectMR
error

            
         1          
[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
 
   
     
  
       
         
  
0
   
             
   
          
               
 0
               
              
              

            
 

    


     
  



             
 

 11
-times
0 11
-times
             
   0      1     

    0    
         
    1       
       














01

                
               

              01
                 
               
    
        
                    
 §                   
                 
                     
                 
        
            

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    
§
b
1
b
2
. . .
b
n2
b
n1
b
n
. . .
find non-empty
 The machine nds the rst non-empty cell.
§
b
1
b
2
. . .
b
n2
b
n1
b
n
. . .
shift left b
n
 The machine shifts the content of each cell one cell to the left
§
b
1
b
2
b
3
. . .
b
n1
b
n
. . .
shift left b
1
 until it reaches the end of tape symbol §.
§
b
1
b
2
b
3
. . .
b
n1
b
n
. . .
find __
 The machine nds two consecutive blank cells and starts over.
               
      




    
   
    
             


             

           
 
 
           


   
               
             
 
   
   
  


 

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
        
   
  0  

  
  
   
 
 
 
           
             
               
               
     
            
     


   
§ 
__ 
__
              
        


   
                 
        
§ 
_

_

_

    
         
           
    
             
         
             
           
         
 
      
      
    
 

             
   1           1 
   
   

      1   1  
           

   
  

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    
             
             
         
     

   
§



_
               
                
                
 
§

_
               
 
                 
             
             
        




  
 
         
          

    
              
           
                  
               




 
          
   1          1  
   
              
         
           
                  
             
 
              


[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
           1
-- start by entering the "check" state
check1 "start" '§' = ("check", '§', 1 )
-- if you read a 1, check that the next cell is blank, and accept
check1 "check" '1' = ("check_blank", '1', 1 )
check1 "check_blank" '_' = ("accept", '_', -1)
-- if either of these conditions is not the case, reject
check1 "check" b = ("reject", b, 1 )
check1 "check_blank" b = ("reject", b, 1 )
-- accepting and rejecting actions
check1 "accept" 1 = ("halt", 1, -1)
check1 "reject" b = ("error", b, 1 )
check1 _state _char = ("error", '_', 0 )
             
        10  01  
           
             
            
            1
              
          1      
    

    


10100
0
0
0
0
0
           
        1      0    
        
     
      
      

     

    
   
   

     
           
               1     
         
 

       0           
               
  
            
            1       
       
             
1
    
       
    

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    
          
   
           
  
       1  0        

halt


1.1.2 Church-Turing thesis and the halting problem
              
           
2
            
  
             
  
              
      
               
                 
                  
            
            
       
 
                
                   
               
3
             
           
        
              
                 
             
             
     
              
   

1   
0     
2
             
3
        

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
                      
 
4
     
     
      1     
       

   
              
         
 
             
        
               
          

 
             
     

   
       
  
    

4
                
       

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    
 
            
                
             
       
  
    
   
 

 
  
   

  

  
        
          

  
           
       
  
  
   
      
       

     

    
               
          
       
  
   

              
        
    
 
1.2 Prerequisites from model theory
           
            
               
       
1.2.1 Formulae and models
            
            
            
              
               
             
    
   
                
           
     



[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
   
         
  
   
     
 
 
       

        
     
     
     
    
    


1
e
    
1
 
    e   
      

01
     
   01  
             
              
 
      
        
 
   
 
    
 
   
   


   
         
           
              
          
 

        
  


1
e
       
 
1
e

   
1
 
  e
      

0  0 
     

  
        
0
1


     0
1
       
    

       

 
   


     



[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    
       

               
 
         
  
     
    x
1
x
2
x
3
  
 
   
     
  x
1
x
1
x
2
x
2
1 

     
         
x
1
x
1
x
2
x
2
1
              

                 
             

  
     
  
       
   x
1
x
n
      x
1
x
n
 
  
  x
1
x
n
  
  x
1
x
n


 
  x
1
x
n
x
i
 

      
  x
1
x
n
   
x
1
x
n

x
1
x
n

x
1
x
n

   
  
x
1
x
n

x
1
x
n








                 
                
                
 
          

    
          

  

          
    
     0  1       


[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
  x
i
 

 
  




      

       
    
            

             


1 1 1
-times
       
01 1 1
-times
  


 

   
    
a
 a              

   
m
1
m
k
 m
i
   
  
        





               

 
     
            
  
     

   
 

5
   

     

               
   
        
 
     
 
5
                 
                    


[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    
               
 
       
 
      
 

 
  
   

             
 
                

6
              
        

   
    


 x
1
x
2
x
3
 x
2
x
1
x
2
1
 x
1
x
2
x
3
x
1
x
2
x
3
x
1
x
3
x
2
x
3
       
 x
1
 x
2
 x
3
 x
1
    x
2

       
             
          

     
        x
1
x
2
 x
3
      
     
           
            
         
      x
1
x
2
 x
3
     x
2
 
  x
1
              x
1
x
n
       x
1
x
n
  
            
x
1
x
n
 
    
    

 

       
 
  
 




6
              x
1
x
1
x
1
     
 

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
  

    

 






     
 
  
  
  
 
 




  x
1
x
n
x
1
x
n
 
   
  
               
       
                
 x
2

x
2
x
1
x
2
x
2
x
2
x
3
x
1

                 
                
                 
              
x
2
x
1
x
2
x
2
x
4
x
3
x
1

          
              
          
1.2.2 Morphisms, theories, and decidability
             
           
              
      
  
      
       
 




    





   

 
 
        

   
      

      
    
 

          
 
       



[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    
       

     

         

             
      
   
       
          

                
     
              
      
           

   
   
x
1
x
1
e x
1
x
1
e
x
1
x
1
x
1
x
2
x
3
x
1
x
2
x
3
x
1
x
2
x
3

x
1
x
1
x
1
1
e
x
1
x
1
1
x
1
e
            
  

 
          
x
1
x
1
0x
2
x
1
x
2
1
     
             
             

 
  

 

   

       
 

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
            
         
      
                
                
     
              
         
          
       
Th
  
    
        
H10

x
i
1
x
i
k
x
i
1
x
i
k
  
          
        
Th



x
i
1
x
i
k

x
i
1
x
i
k

is atomic for , and 
           
              
     

    
x
1
x
1
0x
2
x
1
x
2
1
       Th 
   
      Th
  x
1
x
2
1
1 0         

      H10
     
  H10

     


1
2
4
3

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    
            
          
x
1
x
2
x
3
Ex
1
x
2
Ex
2
x
3
Ex
3
x
1

    x
1
    x
2
x
3
      Th


            
                 
       

    
    

        

         
           


c
         
    
   c
 
             


       


  
 
  
       
H10

x
i
1
x
i
k
x
i
1
x
i
k
  
     
    
        



x
i
1
x
i
k

x
i
1

x
i
k

is atomic for , and 
       
   
       


there exists an atomic formula with
, or and 
  
    
    
                 
   
          



[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
       
      

 
P

       
  

P 

     P  
H10   
    
          


          
    

    
       


  
     
c
x
i
1
x
i
d
             
       
  P      P    
  
x
i
1
x
i
k
x
i
1
x
i
k


     
      
 
 
        

    

 
     
       
 
 
x
i
1
x
i
k
x
i
1
x
i
k
0
 x
i
1
x
i
k
        
  H10           
x
i
1
x
i
k

x
i
1
x
i
k
x
i
1
x
i
k

 

               
 

 





        
  

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    
                
                  
            
         
x
                
   
           
 x
j
   
x
-times
    
s


   
x







   
              
            
      

               
   


x
1
x
1
0
        
x
0 1
     
       
s 
   






    
            

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
H10
(𝔄)
Th
∃+
(𝔄)
Th(𝔄)
𝐷(𝔄)
H10(𝔄)
𝐷
∃+
(𝔄)
𝐷
𝑐
(𝔄)
                  
  
  

  
              
      
               
                   

Th
 
H10

x
i
1
x
i
k
x
i
1
x
i
k
 
Th



x
i
1
x
i
k

x
i
1
x
i
k

is atomic for 



 
H10

x
i
1
x
i
k
x
i
1
x
i
k
 




x
i
1
x
i
k

x
i
1
x
i
k

is atomic for 



there exists an atomic formula with
, or 
            
          
 
ThH10
Th


H10


  
  
ThH10
Th


H10


 
         

0 1

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    
H10
(𝔒
𝐾
)
Th
∃+
(𝔒
𝐾
)
Th(𝔒
𝐾
)
𝐷(𝔒
𝐾
)
H10(𝔒
𝐾
)
𝐷
∃+
(𝔒
𝐾
)
𝐷
𝑐
(𝔒
𝐾
)
𝒦
      
      


          

 


              
               
                   
        
     
    
        
     
 Th


    H10

 


  
 H10

              
        


    
                
        
1.2.3 Computable structures and decidable models
                
            
               
             
             
              
      
 
       


   
         
             
               
            

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
        
   ar    
                  
            
    
            
        
          
  

          
            
       
              
 
               
                
   
              
            
             
           
            
             
   FC    R  
F


       
R


       

C
            
     
            
  
   
            
  

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    
         


     
  
           
  

 


       
 

     
      
    


  
            
  
       

       
 


    

    


    
    
             
             
           
  
               
   
    
    
     
      

     
          
     
 
           
             1
            
  

            

               
 1              
              
11011
   0   1     1
          

 
  
    

       
  
   
  
     


[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
               
           
       

 
          
      

      
           
          
          
            
              
    
             
             
             
 
  
      

  

 
 
  

        
               
             
     

        
                
             
          
                
              
          

                 

       
  

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    
         











     
  

       

 
      
           
     
  
          
             
         

 
   
 
      
         0

0

  
c
n1

c
n

1

 c
n
       
              
              
     
          

 
   H10 
   
         
    
  
  x
1
x
n
x
1
x
n
   
 
     
   
  



             

 

  
      H10    
1.3 Prerequisites from number theory
1.3.1 Number elds and rings of algebraic integers
               
               
               
               
         

             

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
              
        
    
 
  
    

       





   

 
           
              
           
            
             
 



         

       


 



      
               
             

           
  

         
     

    
                
             
 
            
                 


   


         
               
   
                 
              
   
              
   
          

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    
           
            
  
           
            




            
         

   
    
     
 
   



      
    
  

 
       
 

     
            




  
 







  
               
     
           
    
 
               

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
 
  
               
               
          
  
   
          
    
      
 
        
                
      
     
     
            
            
      
      
    
      
     
     
         


 
 
   

     
   
         



   
      
   

  
  

  


    
 
           
   
               


           


     

      






 
 
        
              
    
            
   
    

 
       

       
    


 
               
   
            

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    
 

     


      



           

   
           

  
     
              
              

        




 




           
             
  
    

       
   
              
        
             
         
     

  
 
         
         
    
              
             
         

    
             
            







                
  
  

 

     
              
      

 

  
  
  




  
      
       


  
 

    
  

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
    



  
          
     
     

 
          
        
   
  

         

            

             
               
                  
        
      
       
      
     

    


    
         
          
  
          
  
1.3.2 Ideals of
           
           

  
             
     
  



 

      
7
              
           

 








     
7
           

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    
         


         
       
    
                 
                 
   
               
             
            







                     
            

          

  
  
               
   
            
           

          
            
 

     
       
               
         
       
     
                
           
        

              

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
   













   





               
           
  
            
           
 

             
  

prime ideal
 
          
8
 
          

prime ideal


prime ideal
       

prime ideal


        
       

 
    
8
            
      

                  
   
  
       

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    
   

              
     
   
    

      



   


 


   

          
                
 

 
    






 

   


  

   

 

      

           






   


       




      




       
 


    
         



    
        

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
 
          
    



                



 


      

    
  
   
 

 
               
               
 

           

 
   
 



  
   
           

prime ideal

       
           
                



     
        
      
       
       
              
            

               
1.3.3 Geometry of numbers
               
                

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    
𝐷
𝑒
1
𝑒
2
   
   
            
          

          



            
   
 
       
   
 
            


  
      


 

             
         
9

   
 


  


  


              
                
      
      
          
                  
     
        


9
      
       
             

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
            
         


    
        
    

         
 
 


           

          

 
    
    
      




              





     
   
     







       
             


 
        
  
               
                
        

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    
  
   
  
     
  



  

    
               
      


  
     
         
     
       

              
     

























             
             
      
  


  

      
     
   
    
      
        

  

              

   
    
             
     
            

      
       
          

 
    

         

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
    
            

    



          
     







 
          




   
          

  
        
       
  
             
               
             
   



  
                
  
              

             

             
          
             
 


           

        
   



     
    

                
               
       
 








[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    

     





   
          
  

 







   

   
  








       







     
      





             
 
       
               
                
            
       
         
       


   




         
     
              
              
            
          
           
            
                 

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
       

 
10
       
     
           


          
  





          

       

     

      


           
            
              
            
              
           
                 
              
               
    

  
           
                 
         
        
          
 

10
    

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    
ႼႵᆡ
ႼႴᆡ ႼႳᆡ
ႼႲᆡ Ⴒᆡ
Ⴓᆡ Ⴔᆡ
Ⴕᆡ
ႼႴᆡ
ႼႳᆡ
ႼႲᆡ
Ⴒᆡ
Ⴓᆡ
Ⴔᆡ
          
0
1
;
0 + = 1 +
                   
 

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   

          

                


           
      
    


 


               
            

   
        



      
             
          






             



[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    
      

   
          
        
    
       

  

    
     
       

           

      
 

             
 
    
        
   
    

    

 
    
    
 
 
      
           
 
      
    

 


             
   
               
               
               


[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
          
 
  

  

     
 
       
  
            
 



   

 


          

  

   

  



  




    

       
     

    
 




[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    
       






   



     
     

     
   

     





               
           
 

 

   

  

   



  
 

 

      

      


          
1.3.4 Absolute values and local elds
              
              
              

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
          
       
    
  
    
 
        
       
    
            

   
  

  
           
      
 
  
         

    
          





 

              

   
 
    
      
 
             
 

           
  
   
     
    
 


   
        

         

                
                
              
            
    
       
       

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
    
  
            
          


                
            
             
              
             
           
           
   


  
  
 

         
              
   

      







 
 

   

         
 

   
     
           
        
              
                 
               
             
          
         
  
       


  
    
 

       

  
             

          

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
      
 
 
                
         


      



  
      
         
 
       

    



           

     
       
   
          

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
2 Hilbert’s tenth problem
2.1 Dierent perspectives on an old problem
2.1.1 Diophantine equations and sets
              
        
1
   
                
               
   
        
           
              
           
2

       



 

       

                 
                
       
3
     
                  
                
      
    
    
  1 
   0 
              

 
                 
0  1              
     
1
 
2
           
             
                  
   
3
     

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  
         
               

   1      0 
               
α  α              
  
         

          

          

  
             

              
       
     
    


 
 







 

       


 


   
      

 






                
 
            
 
  
     
 
          
           
          
  

           
 
               
              
   




[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
      
𝑥
2
+ 𝑦
2
= 1
−1 𝑥 1
         
    
          

 
 
     





     

    

 
         
  

     
     
 

          


                

           
   
      
 



              
   



 


         



     


 


[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  
    

 
    
     
 

               
      

                
               
          
          
                 
   
          
          
    
       
      









  
 

      



 

     

  




    
  

  


            
       

            
              

       


 





[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
      
                  









         
               




  

       




            
  

    




















       























         
    

              
           

 
        
 x
1
x
n
y
1
y
m
 

y
1
y
m

y
1
y
m

      
        
     

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  
              
                
              
         H10     
     
     H10
               
     
             
 
   

             
      

            
           
  
   
  
 
  


       
  
      



      
 

            

   

   



            
      


         


  
        



  


  
  
 






[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
      
    
 
    
 

    



 
 








           
 
 







                  
 
           
             
           
              
             
      
  
         
       
           
 
      
 

             
             
               


        

 


   H10
             

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  
              
         
   
  
   
              
       
     
        
   
             
            
2.1.2 Purely Diophantine sets
       
     
     


  
 







         
             
               
         
           

 
         

 x
1
x
n
y
1
y
m
 

y
1
y
m

y
1
y
m

               
               
        
                 
           
  
               
            

              
          
  
          
             
       
             
         

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
      
            
                
          
        
                
        
  
   
    

      

 



   
            
   
             
          
 


    
  
           
 
 

         
   

         
            
      



  
      
  




    


     




                
     
    

 
     
 
             
         
        


[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  
             
     
      
  
         
             
  
     

  
         
 

       
 





           
  
               
  
   
 
  
     





 
     
     
        




          
  

      
 
 

 





             
 
  


       





[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
      
H10
(𝔒
𝐾
)
Th
∃+
(𝔒
𝐾
)
Th(𝔒
𝐾
)
𝐷(𝔒
𝐾
)
H10(𝔒
𝐾
)
𝐷
∃+
(𝔒
𝐾
)
𝐷
𝑐
(𝔒
𝐾
)
𝒦
             










           

 

    
       
           



    

     

     
   
 
   
  




 
          

    
               
        
              H10

        
2.1.3 Related problems
                 
             
             

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  
Th     
4
        
              
          
   
     Th
        
            
            
 
           
   
                 
            
        H10    
  
              
         



            
  

          
     
      

    
            
         


   
 


      

y
1
y
m

y
1
y
m

   H10        
        H10
     H10    
4
                 
           

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
                
               
 
               
             
              
                
               
             
                
            

   
              
    
              
 
2.2 Some structural results
             
              
 
  
        
 
 
 

   

 

      
  
    
  

     

 

 
    



         
    

 

    
              
                
   
           
           H10 
  

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  
            
           
          
               
         
         

 


 
             
     H10
     
         
                 
 
     
       
    
              
   
         
 H10


           

             
           
    
         
           

               
 H10

       
                
       
 
        
      
  
         

  
 
       101 
       
 

-times
  

-times
 

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
              
      

   

    
 
       












               
    
         
          


















   





















       
    
               

                 
          
  
   
          
          
    

     
             
                  
          
           







  





   

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  



        
         
   
  







      












   
       
       
          
   
   
     




 




 
  

  


     









  







 












     





     

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
   
       


      
 
  
    




 
               
              
   
    





       
        
      
       
   


   
  



      
  











       

  



    
 



     

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  
        





     





     


       








               
            
  
       
    
    
    





        


  












    
           
         
   
   
       
     
       

        
 
     
    
 
  
   

             

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
              
  


                
   
        



      


         
2.3 Hilbert’s tenth problem over totally real number elds and
number elds with one pair of non-real embeddings
                
                
              
                
                  
             
2.3.1 Finitely many easy lemmas
          

               
     
  
 
      
      
  
     
   







[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  
     
      
          

    
 

      

    


          
 
              
  

       
  
              
  


     
      
      
       

 
  
           
 
 
          
    

 

      
 


   



 
          



even


odd


    

even


[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
              


odd


               
     
        
   
  
   



       

   
 
       

  
          
   
 


 





  








     









 
  

         



    
           
        



        

 
 
        
    
  

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  






  




       

 


  
 
 

 
  
     



 







 


  



 
      



             

       
     
   










    
 
   
 
               



            


 


     







[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
              



odd


         
   

   

 
  
       


       

        
               


           
          
      
    
    







      
   
      




 







         
       
     
    

 
    

 

 
             
 
       


                
  

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  
       



 
 
           

  
          









 
 

 
      
    
      



            


    









          
                 
    
       
     
      



         
               
  













       
     
    


[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
              
     
      


 
   
 
       


    

 
 
    

      



    

   

 
    




    
       

 
   

 
 
       
   


       
 


 
   

     
            
 


 


 



     
     
 
          

    
 
         
 



      
     


    
       



  
  


        



       



   

         
    







[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  
  
   









          
          


  
  


 
    
    


 


 
  
 

      
          
   
 
       


   

    



-times
  

 




     

      


              
     





               

           
   
              
              

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
              
    


 


 
                
                
               
             
   

       
             
            
          
2.3.2 Diophantine denition of over
               
            
    
        
   
               
       


       
  


    


    
   
      
 

     
       
     
         













 
  
   
 

  
    
    
    
   
         

   
        
 


[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  
               
          




     



      

 



 

    
      
         
     

     
 




     















 








      
       

        
     
   

       



 
     
  
        
  



         
     

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
              


       

 



 





 
 
      

   

  
          
   
 
 




    
 
   
       
    
      
    
     

      




            
 

    








          
  
          
   
 
        



 


   

 


                
          











 
  
    
 
  
   
      

           
       


            
   
         
   
    

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  












 



         


       

      

  

 
      
              
    
     
    
 

             
        
        


 

  

            
  
   

 
  
      
 



 

  

 



 
      
 


 

    
      

 











    
  


       

 
    















[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
              
      





  
             
      

    
               
    
    
          



 





 























  

 



   



 
















  



   

          




    
   







    









[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  
               



by (iv)

        




         

 
    


      
       
        
     
     

          
              

                 

            

    
       
     
            
          

   
        
 
  
        
  
    
       
   

        


    



 






          



 






 
 


   



[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
              
  

     
 
    
 






  


       








 
 
            









        




















 
      














































       
    
         
               
 
   



    
      

    

 








[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  
      







   
 












       

      
   
    


    
   
     

    

   

 

         
            

  



     
   



                   
                 
               
     
           

    
    



   
      



      
             
      
 
 


   

     
    
      
        





[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
              
          

even






odd





         

 

       
    
 



     
      
 

  








    

  
  
       
    
      
   








           


    


 



     


  
        
    




         

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  


             

   


 
 




  

       
     


 



   





            
   




















          
     





 

    
  

 


  
  


     


     




     



    


[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
              
   












        
    




 
  
 


     
    
        
  


 
             
 
  
 
         


   

   



  
    


  


 
   









  


    
 



      























[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  
 
    





  



       
 






   
          
 


         
 
   







        




  







         
     
         



 
   


































             

 
  







        


  









































[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
              
      

      








 



       
 


Lem. 2.3.3.(ii)




     


 




    
      

 

   
  
 



    


 
  
      



     
              









even




odd




  

 

     








  

  

 

      
          
  





      

  


  
  
  
 
   
   
   









       

  
  
  

   
  






 
        
   

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  
 

               
 




























             

   
        
















    































     
 

   


  
         























     
   








         







           
  

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
              
 
 








    
  






























      
    
 
  



        








    
     

     
      


     
    




   
    













         















          
   
 
  
      
  

  
 
  

 
 

 
 
             
 









[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  
            


    





   


 
       
        



          











 
             








         
 




    


            
    

  
 












      


      












 
 
 
 
    
   













   
        
  

   
      







  









     
        


 

 
  
            

          
 

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
              

        
  
   
        
 

           

































 


 

 



    
 
 






             
           
  
      
              
    
            
             
              

      

         

       

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  
  













 






 
          
          
 
             
 

 



 



 


 

        



 


 

 

 
 

  
 

 
 
 

 
      
 
    
 


         
 

 
            

 


[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
              
    

 

        
      
  
            

 
          
 


       
 


        







          









               
         

 
         





        

          
 






      
 

      
  
 


 
 

  
     

    


  

    

   

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  
             
 



            
 


 
    



 
   
 

       
  
       



           
        
               
          
       
  
          





             
               
              
                
               
            
            
              
               
         
              
 
        
           
            
  H10
           
            H10
  
               
            

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
A Collected Haskell implementations
A.1 Simulating Turing machines
          https://github.com/
tim6her/h10-turing-machines            
 
git clone https://github.com/tim6her/h10-turing-machines.git
cd h10-turing-machines
cabal setup && cabal build && cabal install
             ghci  
              
             
>>> import Automaton.TuringMachine
>>> :l tally
>>> let d = toTransition tally "error" -- mark the errornous state
>>> let turing = TuringMachine "start" '_' "halt" d
>>> "§1111" >>> turing -- Tally encoding of 4
Just "§1"
>>> "§1011" >>> turing -- Not tally encoded
Just "§0"
            
A.2 Polynomials
            
             
        
         
{-# LANGUAGE RebindableSyntax #-}
module Monomial
( Monomial
, (<*>)
, idt
, mfromList
, clean
) where

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  
import NumericPrelude
import Data.Map (Map, delete, empty, foldrWithKey, fromList, member, insert,
insertWith, (!))
import Algebra.Monoid as Monoid
import Test.Tasty
import Test.Tasty.HUnit
import Test.Tasty.QuickCheck as QC
-- | Monomials are mappings from ZZ to NN with finite support
newtype Monomial = Monomial (Map Integer Integer) deriving (Eq, Ord)
instance Monoid.C Monomial where
idt = Monomial empty
(<*>) = mmul
instance Show Monomial where
show (Monomial m)
| m == empty = "1"
| otherwise = foldrWithKey
(\x e sh -> "X" ++ show x ++ "^" ++ show e ++ " " ++ sh)
"" m
-- | Creates monomials from list of tuples
--
-- Left entry is index of indeterminate, right index is power of the
-- indeterminate
--
-- === Example
-- >>> mfromList [(1, 2), (0, 3), (4, 7)]
-- X0^3 X1^2 X4^7
mfromList :: [(Integer, Integer)] -> Monomial
mfromList l = clean $ Monomial $ fromList l
-- | Multiplies two monomials
--
-- === Example
-- >>> mmul (mfromList [(1, 2), (2, 4)]) (mfromList [(2, 1), (3, 2)])
-- X1^2 X2^5 X3^2
mmul :: Monomial -> Monomial -> Monomial
mmul xx@(Monomial m1) yy@(Monomial m2)
| m1 == empty = yy
| m2 == empty = xx
| otherwise = clean $ Monomial $ foldrWithKey

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
 
(\x e m -> if x `member` m
then insertWith (+) x e m
else insert x e m)
m2 m1
clean :: Monomial -> Monomial
clean (Monomial m)
| m == empty = (Monomial m)
| otherwise = Monomial $ foldrWithKey
(\x e m -> if e <= 0
then delete x m
else m)
m m
-- * Testing
main :: IO ()
main = defaultMain tests
tests :: TestTree
tests = testGroup "Tests" [properties, unitTests]
properties :: TestTree
properties = testGroup "Properties" [qcProps]
qcProps = testGroup "Axioms of monoids"
[ QC.testProperty "left multiplication by identity" $
\x -> (let m = mfromList (x :: [(Integer, Integer)])
in idt <*> m == m)
, QC.testProperty "right multiplication by identity" $
\x -> (let m = mfromList (x :: [(Integer, Integer)])
in m <*> idt == m)
, QC.testProperty "associativity" $
\x y z -> (let m1 = mfromList (x :: [(Integer, Integer)])
m2 = mfromList (y :: [(Integer, Integer)])
m3 = mfromList (z :: [(Integer, Integer)])
in (m1 <*> m2) <*> m3 == m1 <*> (m2 <*> m3))
, QC.testProperty "commutativity" $
\x y -> (let m1 = mfromList (x :: [(Integer, Integer)])
m2 = mfromList (y :: [(Integer, Integer)])
in m1 <*> m2 == m2 <*> m1)
]
unitTests = testGroup "Unit tests"
[ testCase "show X0^3 X1^2 X4^7" $
show (mfromList [(1, 2), (0, 3), (4, 7)]) @?= "X0^3 X1^2 X4^7 "

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  
, testCase "sample multiplication" $
show (mmul (mfromList [(1, 2), (2, 4)]) (mfromList [(2, 1), (3, 2)])) @?=
"X1^2 X2^5 X3^2 "
, testCase "test clean" $
mfromList [(1, 0), (2, 0), (3, 1)] @?= mfromList [(3, 1)]
]
         
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
import NumericPrelude
import qualified Monomial
import qualified Data.Map as Map
import Algebra.Monoid as Monoid
import Algebra.Ring as Ring
import Algebra.Module as Module
import Algebra.Additive as Additive
import Test.Tasty
import Test.Tasty.HUnit
import Test.Tasty.QuickCheck as QC
-- | Polynomials over a ring R are finitely supported functions
-- from the set of monomials to R
newtype Polynomial a = Polynomial (Map.Map Monomial.Monomial a)
-- | Polynomials form an additive (abelian) group
instance (Ring.C a, Eq a) => Additive.C (Polynomial a) where
zero = Polynomial Map.empty
(+) = padd
negate (Polynomial m) = Polynomial $ Map.map negate m
-- | Polynomials from an R-module
instance (Ring.C a, Eq a) => Module.C a (Polynomial a) where
(*>) 0 _ = zero
(*>) a (Polynomial m) = Polynomial $ Map.map (a*) m
-- | Polynomials form a ring with unit
instance (Ring.C a, Eq a) => Ring.C (Polynomial a) where
one = pfromList [(1, [])]
(*) p@(Polynomial m1) q
| p == zero = zero
| q == zero = zero

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
 
| p == one = q
| q == one = p
| otherwise = Map.foldrWithKey
(\mono coeff poly -> (coeff *> mono `mmul` q) + poly)
0 m1
-- | Two polynomials are equal if their difference is zero
instance (Ring.C a, Eq a) => Eq (Polynomial a) where
(==) p q = let (Polynomial m) = p - q in m == Map.empty
instance (Show a, Eq a) => Show (Polynomial a) where
show (Polynomial p)
| p == Map.empty = "0"
| otherwise = Map.foldrWithKey
(\m a sh -> show a ++ " " ++ show m ++ "+ " ++ sh)
"" p
-- | Adds two polynomials over the same ring
--
-- If a coefficient of a monoid equals 0 the monoid is dropped out of the map
padd :: (Ring.C a, Eq a) => Polynomial a -> Polynomial a -> Polynomial a
padd p@(Polynomial m1) q@(Polynomial m2)
| m1 == Map.empty = q
| m2 == Map.empty = p
| otherwise = clean $ Polynomial $ Map.foldrWithKey
(\mono coeff poly -> if mono `Map.member` poly
then Map.insertWith (+) mono coeff poly
else Map.insert mono coeff poly)
m2 m1
mmul :: (Ring.C a, Eq a) => Monomial.Monomial -> Polynomial a -> Polynomial a
mmul mono poly@(Polynomial mp)
| mono == Monomial.idt = Polynomial mp
| poly == zero = zero
| otherwise = Polynomial $ Map.mapKeys (mono Monomial.<*>) mp
-- | Generate polynomials from lists
pfromList :: (Ring.C a, Eq a) => [(a, [(Integer, Integer)])] -> Polynomial a
pfromList [] = zero
pfromList ((a, m):l) = deepClean . clean $ (Polynomial $ Map.singleton
(Monomial.mfromList m) a) + pfromList l
-- | Comfort function for creating polynomials
--
-- === Example

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  
-- >>> 2 *> ((x 1 + x 2) * (x 1 - x 2)) == 2 *> x 1 ^ 2 - 2 *> x 2 ^ 2
-- True
x :: (Ring.C a, Eq a) => Integer -> Polynomial a
x i = pfromList [(1, [(i, 1)])]
-- | Remove monoids with coefficient zero from support
clean :: (Ring.C a, Eq a) => Polynomial a -> Polynomial a
clean (Polynomial m) = Polynomial $ Map.foldrWithKey
(\mono coeff poly -> if coeff == 0
then Map.delete mono poly
else poly)
m m
-- | Remove variables with power zero from monomials
--
-- This function runs in O(n log(n)) so use it sparsely
deepClean :: (Ring.C a, Eq a) => Polynomial a -> Polynomial a
deepClean (Polynomial m) = Polynomial $ Map.mapKeys Monomial.clean m
-- * Testing
main :: IO ()
main = defaultMain tests
tests :: TestTree
tests = testGroup "Tests" [properties, unitTests]
properties :: TestTree
properties = testGroup "Properties" [qcAddProps, qcModProps,
localOption (QuickCheckTests 5) qcRingProps,
qcAlgebraProps]
qcAddProps = testGroup "Group axioms for addition"
[ QC.testProperty "addition is commutative" $
\x y -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
q = pfromList (y :: [(Int, [(Integer, Integer)])])
in p + q == q + p)
, QC.testProperty "addition is associative" $
\x y z -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])
p2 = pfromList (y :: [(Int, [(Integer, Integer)])])
p3 = pfromList (z :: [(Int, [(Integer, Integer)])])
in (p1 + p2) + p3 == p1 + (p2 + p3))
, QC.testProperty "addition by zero" $
\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in p + zero == p)
, QC.testProperty "addition with inverse" $

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
 
\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in p - p == zero)
]
qcModProps = testGroup "Module axioms"
[ QC.testProperty "first distributive law" $
\a x y -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
q = pfromList (y :: [(Int, [(Integer, Integer)])])
in (a :: Int) *> (p + q) == a *> q + a *> p)
, QC.testProperty "second distributive law" $
\a b x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in (a + b :: Int) *> p == a *> p + b *> p)
, QC.testProperty "multiplications commute" $
\a b x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in (a * b :: Int) *> p == a *> (b *> p))
, QC.testProperty "multiplication by one" $
\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in (one :: Int) *> p == p)
]
qcRingProps = testGroup "Ring axioms"
[ QC.testProperty "multiplication is associative" $
\x y z -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])
p2 = pfromList (y :: [(Int, [(Integer, Integer)])])
p3 = pfromList (z :: [(Int, [(Integer, Integer)])])
in (p1 * p2) * p3 == p1 * (p2 * p3))
, QC.testProperty "left multiplication by one" $
\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in one * p == p)
, QC.testProperty "right multiplication by one" $
\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])
in p * one == p)
, QC.testProperty "distributive law" $
\x y z -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])
p2 = pfromList (y :: [(Int, [(Integer, Integer)])])
p3 = pfromList (z :: [(Int, [(Integer, Integer)])])
in p1 * (p2 + p3) == p1 * p2 + p1 * p3)
]
qcAlgebraProps = testGroup "Algebra axioms"
[ QC.testProperty "multiplications commute" $
\x y a -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])
p2 = pfromList (y :: [(Int, [(Integer, Integer)])])
in (a :: Int) *> (p1 * p2) == (a *> p1) * p2)
]

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
  
unitTests = testGroup "Unit tests"
[ testCase "sample polynomial" $
show (pfromList [(1, [(1, 2), (3, 4)]), (-4, [(1, 4), (2, 3)])]
:: Polynomial Int) @?= "1 X1^2 X3^4 + -4 X1^4 X2^3 + "
, testCase "test equality" $
pfromList [(0, [(1, 1)])] @?= (zero :: Polynomial Int)
]

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
B Summaries
B.1 Zusammenfassung
            
          
                
            
            
              
            
            
             
           
     
            
          
           
             
          
             
          
            
           
         
       
     
        
 
     
              
          
           
   
        
 
           
              
    
    

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56

B.2 Summary
              
             
                 
             
                
               
               
              
                

            
                
              
              
           
              
              
              
               
       
   
 
           
              
                
               

        
   
                
             
       

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
List of Figures
      
  
    
add1
 1101
             
  
               
        
             
        
     
     
 



  
    
          
                
      
         
           



[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56
Bibliography
         
         
   
             
       http://www.jstor.org/stable/2269326
            
        10.2307/2371045
           
   
           
          10.2307/2318447
 http://www.jstor.org/stable/2318447
             
        10.1016/j.amc.2005.09.066 
https://doi.org/10.1016/j.amc.2005.09.066
          
        
          
             
 
              
       10.2307/1998133
              
       10.2307/2040720
             
            
10.1112/jlms/s2-18.3.385
               
        
10.1515/crll.1988.388.189  https://doi.org/10.1515/crll.1988.388.189
             
      10.1112/jlms/s1-8.1.18

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56

            
          
   
            
            
          
            
  10.1007/BF01700692  https://doi.org/10.1007/BF01700692
             
     
            
           
 10.1090/S0273-0979-00-00881-8
         
         
       
          
           
       
10.1007/978-3-642-75306-0
          
           
            
            
     10.1215/S0012-7094-36-00227-2 
https://doi.org/10.1215/S0012-7094-36-00227-2
           
          
         
  10.1007/978-3-642-54936-6_5
            
       10.1007/978-1-4613-0041-0 
https://doi.org/10.1007/978-1-4613-0041-0
             
    
            
            
https://www.ebook.de/de/product/3665990/david_marker_model_theory_an_
introduction.html

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56

          
        
          
www.jmilne.org/math/
           
    http://www.logic.univie.ac.at/~muellem3/TCS.pdf  

        
    
             
         
http://ubdata.univie.ac.at/AC05622932
             
           
10.4310/MRL.2013.v20.n5.a12
              
          10.2307/2047021 
https://doi.org/10.2307/2047021
           
         
http://www.ams.org/notices/200803/tx080300344p.pdf
             
           
             
10.1007/3-540-45455-1_4
             
           
10.1090/S0002-9904-1944-08111-1 
https://doi.org/10.1090/S0002-9904-1944-08111-1
            
          10.2307/2266510
             
         10.2307/2033628 
https://doi.org/10.2307/2033628
            
        10.2307/2266685
             
       10.2307/2269028

[git] Branch: master @ 1f9ef90 Head tags: v0.6-1-g1f9ef90 Compile time: 2019-09-08 17:56

               
        10.1515/crll.1986.368.127

https://doi.org/10.1515/crll.1986.368.127
         
             
  10.1002/cpa.3160420805 
https://doi.org/10.1002/cpa.3160420805
           
            
10.1002/cpa.3160420703
           
           
          
https://doi.org/10.1090/conm/270/04370
           
          
     
http://www.ebook.de/de/product/6433593/alexandra_shlapentokh_hilbert_s_
tenth_problem_diophantine_classes_and_extensions_to_global_fields.html
         
http://math.cornell.edu/~shore/papers/pdf/proc4t.pdf   
           
            
          
10.1016/S0049-237X(99)80028-7 
http://www.sciencedirect.com/science/article/pii/S0049237X99800287
            
      http://eudml.org/doc/212515
           
           
  10.1112/plms/s2-42.1.230 
https://doi.org/10.1112/plms/s2-42.1.230
